1 /-
2 Copyright (c) 2019 Scott Morrison. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Scott Morrison
5 -/
6 import algebra.category.Mon.basic
src └────────────────────────┘
7 import category_theory.limits.limits
src └───────────────────────────┘
8
9 /-!
10 # The category of monoids has all colimits.
11
12 We do this construction knowing nothing about monoids.
13 In particular, I want to claim that this file could be produced by a python script
14 that just looks at the output of `#print monoid`:
15
16 -- structure monoid : Type u → Type u
17 -- fields:
18 -- monoid.mul : Π {α : Type u} [c : monoid α], α → α → α
19 -- monoid.mul_assoc : ∀ {α : Type u} [c : monoid α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
20 -- monoid.one : Π (α : Type u) [c : monoid α], α
21 -- monoid.one_mul : ∀ {α : Type u} [c : monoid α] (a : α), 1 * a = a
22 -- monoid.mul_one : ∀ {α : Type u} [c : monoid α] (a : α), a * 1 = a
23
24 and if we'd fed it the output of `#print comm_ring`, this file would instead build
25 colimits of commutative rings.
26
27 A slightly bolder claim is that we could do this with tactics, as well.
28
29 Because this file is "pre-automated", it doesn't meet current documentation standards.
30 Hopefully eventually most of it will be automatically synthesised.
31 -/
32
33 universes v
34
35 open category_theory
36 open category_theory.limits
37
38 namespace Mon.colimits
39
40 variables {J : Type v} [small_category J] (F : J ⥤ Mon.{v})
id └────────────┘ ┴ └─┘
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴ └─┘
doc └────────────┘ ┴ └─┘
41
42 inductive prequotient
43 -- There's always `of`
44 | of : Π (j : J) (x : F.obj j), prequotient
id └──┘ ┴
src └──┘
typ └──┘ ┴
45 -- Then one generator for each operation
46 | one {} : prequotient
47 | mul : prequotient → prequotient → prequotient
48
49 open prequotient
50
51 inductive relation : prequotient F → prequotient F → Prop
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
52 -- Make it an equivalence relation:
53 | refl : Π (x), relation x x
id ┴ ┴ ┴
typ ┴ ┴ ┴
54 | symm : Π (x y) (h : relation x y), relation y x
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
55 | trans : Π (x y z) (h : relation x y) (k : relation y z), relation x z
id ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
56 -- There's always a `map` relation
57 | map : Π (j j' : J) (f : j ⟶ j') (x : F.obj j), relation (of j' ((F.map f) x)) (of j x)
id ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └──┘ ┴ ┴ └┘ ┴ ┴
src ┴ └──┘ └┘ └──┘ └┘
typ ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └──┘ ┴ ┴ └┘ ┴ ┴
58 -- Then one relation per operation, describing the interaction with `of`
59 | mul : Π (j) (x y : F.obj j), relation (of j (x * y)) (mul (of j x) (of j y))
id ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ └┘ ┴ └─┘ └┘ └┘
typ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴
60 | one : Π (j), relation (of j 1) one
id ┴ └┘ ┴ └─┘
src └┘ └─┘
typ ┴ └┘ ┴ └─┘
61 -- Then one relation per argument of each operation
62 | mul_1 : Π (x x' y) (r : relation x x'), relation (mul x y) (mul x' y)
id ┴ └┘ ┴ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
src └─┘ └─┘
typ ┴ └┘ ┴ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ └┘ ┴
63 | mul_2 : Π (x y y') (r : relation y y'), relation (mul x y) (mul x y')
id ┴ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘
src └─┘ └─┘
typ ┴ ┴ └┘ └──────┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘
64 -- And one relation per axiom
65 | mul_assoc : Π (x y z), relation (mul (mul x y) z) (mul x (mul y z))
id ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
66 | one_mul : Π (x), relation (mul one x) x
id ┴ └─┘ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴
67 | mul_one : Π (x), relation (mul x one) x
id ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ └─┘ ┴
68
69 def colimit_setoid : setoid (prequotient F) :=
id └────┘ └─────────┘ ┴
src └────┘ └─────────┘
typ └────┘ └─────────┘ ┴
70 { r := relation F, iseqv := ⟨relation.refl, relation.symm, relation.trans⟩ }
id └──────┘ ┴ └───────────┘ └───────────┘ └────────────┘
src └──────┘ └───────────┘ └───────────┘ └────────────┘
typ └──────┘ ┴ └───────────┘ └───────────┘ └────────────┘
71 attribute [instance] colimit_setoid
id └────────────┘
src └────────────┘
typ └────────────┘
72
73 def colimit_type : Type v := quotient (colimit_setoid F)
id └──────┘ └────────────┘ ┴
src └──────┘ └────────────┘
typ └──────┘ └────────────┘ ┴
74
75 instance monoid_colimit_type : monoid (colimit_type F) :=
76 { mul :=
77 begin
78 fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
id └───────┘ └──────────┘ └──────────┘ ┴
src └─────┘ └───┘ ┴ └┘ ┴ └──────────┘┴ └┘
typ └─────┘ └───────┘└───┘ └──────────┘┴ └┘ ┴ └──────────┘┴┴└┘
doc └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
txt └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
par └─────┘ └───┘ ┴ └┘ ┴ ┴ └┘
pid ┴ └───┘ ┴ └┘ ┴ ┴ └┘
st └───────────────────────────────────────────────────┘└─
79 { intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ─────┘└─────┘└─
80 fapply @quot.lift,
id └───────┘
src └─────┘
typ └─────┘ └───────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ──────────────────────┘└─
81 { intro y,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───────┘└─────┘└─
82 exact quot.mk _ (mul x y) },
id └─────┘ └─┘ ┴ ┴
src └────┘ └─┘ └─┘┴ ┴ └┘
typ └────┘└─────┘└─┘ └─┘┴┴┴┴└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ─────────────────────────────────┘└┘└
83 { intros y y' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────────┘└─
84 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
85 exact relation.mul_2 _ _ _ r } },
id └────────────┘ ┴
src └────┘└────────────┘└─────┘ ┴
typ └────┘└────────────┘└─────┘┴┴
doc └────┘ └─────┘ ┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ └─────┘ ┴
st ────────────────────────────────────┘└──┘└
86 { intros x x' r,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────────┘└─
87 funext y,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ─────────────┘└─
88 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────────┘└─
89 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
90 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
91 { exact relation.mul_1 _ _ _ r },
id └────────────┘ ┴
src └────┘└────────────┘└─────┘ ┴
typ └────┘└────────────┘└─────┘┴┴
doc └────┘ └─────┘ ┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ └─────┘ ┴
st ───────┘└───────────────────────────┘└┘└
92 { refl } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────┘└────
93 end,
st ────┘
94 one :=
95 begin
st └─────
96 exact quot.mk _ one
id └─────┘ └─┘
src └────┘ └─┘└─┘└
typ └────┘└─────┘└─┘└─┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────
97 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
98 mul_assoc := λ x y z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
99 begin
st └─────
100 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
101 induction y,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
102 induction z,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
103 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
104 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
105 apply relation.mul_assoc,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
106 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
107 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
108 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
109 end,
st ────┘
110 one_mul := λ x,
id ┴
typ ┴
111 begin
st └─────
112 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
113 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
114 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
115 apply relation.one_mul,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
116 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
117 end,
st ────┘
118 mul_one := λ x,
id ┴
typ ┴
119 begin
st └─────
120 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
121 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
122 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
123 apply relation.mul_one,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
124 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
125 end }
st ────┘
126
127 @[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl
id └─────┘ └──────┘ └─┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └─┘ ┴ └──────────┘ └─┘
typ └─────┘ └──────┘ └─┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
128 @[simp] lemma quot_mul (x y) : quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
id └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
src └──────┘ └─┘ ┴ └──────┘ ┴ └──────┘ └──────────┘ └─┘
typ └─────┘ └──────┘ └─┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴ ┴ └─────┘ └──────┘ ┴ └──────────┘ ┴ └─┘
doc └──┘
129
130 def colimit : Mon := ⟨colimit_type F, by apply_instance⟩
id └─┘ └──────────┘ ┴
src └─┘ └──────────┘ └────────────┘
typ └─┘ └──────────┘ ┴ └────────────┘
doc └─┘ └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
131
132 def cocone_fun (j : J) (x : F.obj j) : colimit_type F :=
id ┴ ┴└──┘ ┴ └──────────┘ ┴
src └──┘ └──────────┘
typ ┴ ┴└──┘ ┴ └──────────┘ ┴
133 quot.mk _ (of j x)
id └─────┘ └┘ ┴ ┴
src └┘
typ └─────┘ └┘ ┴ ┴
134
135 def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
id ┴ ┴└──┘ ┴ ┴ └─────┘ ┴
src └──┘ ┴ └─────┘
typ ┴ ┴└──┘ ┴ ┴ └─────┘ ┴
136 { to_fun := cocone_fun F j,
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
137 map_one' := quot.sound (relation.one _ _),
id └────────┘ └──────────┘
src └────────┘ └──────────┘
typ └────────┘ └──────────┘
138 map_mul' := λ x y, quot.sound (relation.mul _ _ _) }
id ┴ ┴ └────────┘ └──────────┘
src └────────┘ └──────────┘
typ ┴ ┴ └────────┘ └──────────┘
139
140 @[simp] lemma cocone_naturality {j j' : J} (f : j ⟶ j') :
id ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ └┘
doc └──┘
141 F.map f ≫ (cocone_morphism F j') = cocone_morphism F j :=
id ┴└──┘ ┴ ┴ └─────────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴
src └──┘ ┴ └─────────────┘ ┴ └─────────────┘
typ ┴└──┘ ┴ ┴ └─────────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴
142 begin
st └─────
143 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
144 apply quot.sound,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────┘└─
145 apply relation.map,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
146 end
st ──┘
147
148 @[simp] lemma cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j):
id ┴ ┴ ┴ └┘ ┴└──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ └┘ ┴└──┘ ┴
doc └──┘
149 (cocone_morphism F j') (F.map f x) = (cocone_morphism F j) x :=
id └─────────────┘ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ └──┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
150 by { rw ←cocone_naturality F f, refl }
id └───────────────┘ ┴ ┴
src └──┘└───────────────┘┴ ┴ └───┘
typ └──┘└───────────────┘┴┴┴┴ └───┘
doc └──┘ ┴ ┴ └───┘
txt └──┘ ┴ ┴ └───┘
par └──┘ ┴ ┴ └───┘
pid └┘ ┴ ┴ ┴
st └──────────────────────────┘└─────┘└┘
151
152 def colimit_cocone : cocone F :=
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
153 { X := colimit F,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
154 ι :=
155 { app := cocone_morphism F, } }.
id ┴ └─────────────┘ ┴
src ┴ └─────────────┘
typ ┴ └─────────────┘ ┴
doc ┴
156
157 @[simp] def desc_fun_lift (s : cocone F) : prequotient F → s.X
id └────┘ ┴ └─────────┘ ┴ ┴ ┴└┘
src └────┘ └─────────┘ └┘
typ └────┘ ┴ └─────────┘ ┴ ┴ ┴└┘
doc └──┘ └────┘
158 | (of j x) := (s.ι.app j) x
id └┘ ┴ ┴ ┴└┘└──┘
src └┘ └┘└──┘
typ └┘ ┴ ┴ ┴└┘└──┘
159 | one := 1
id └─┘
src └─┘
typ └─┘
160 | (mul x y) := desc_fun_lift x * desc_fun_lift y
id └─┘ ┴ ┴ └───────────┘ ┴ └───────────┘
src └─┘ ┴
typ └─┘ ┴ ┴ └───────────┘ ┴ └───────────┘
161
162 def desc_fun (s : cocone F) : colimit_type F → s.X :=
id └────┘ ┴ └──────────┘ ┴ ┴└┘
src └────┘ └──────────┘ └┘
typ └────┘ ┴ └──────────┘ ┴ ┴└┘
doc └────┘
163 begin
st └─────
164 fapply quot.lift,
id └───────┘
src └─────┘
typ └─────┘└───────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st ─────────────────┘└─
165 { exact desc_fun_lift F s },
id └───────────┘ ┴ ┴
src └────┘└───────────┘┴ ┴ ┴
typ └────┘└───────────┘┴┴┴┴┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└──────────────────────┘└┘└
166 { intros x y r,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ───────────────┘└─
167 induction r; try { dsimp },
id ┴
src └────────┘ └────┘└────┘┴
typ └────────┘┴ └────┘└────┘┴
doc └────────┘ └────┘└────┘┴
txt └────────┘ └────┘└────┘┴
par └────────┘ └────┘└────┘┴
pid ┴ └────────┘
st ─────────────────────┘└─────┘└┘└
168 -- refl
st ────────────
169 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────┘└───┘└┘└
170 -- symm
st ────────────
171 { exact r_ih.symm },
id └───────┘
src └────┘└───────┘┴
typ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└──────────────┘└┘└
172 -- trans
st ─────────────
173 { exact eq.trans r_ih_h r_ih_k },
id └──────┘ └────┘ └────┘
src └────┘└──────┘┴ ┴ ┴
typ └────┘└──────┘┴└────┘┴└────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────┘└───────────────────────────┘└┘└
174 -- map
st ───────────
175 { rw cocone.naturality_concrete, },
id └────────────────────────┘
src └─┘└────────────────────────┘
typ └─┘└────────────────────────┘
doc └─┘└────────────────────────┘
txt └─┘
par └─┘
pid ┴
st ─────┘└───────────────────────────┘└──┘└
176 -- mul
st ───────────
177 { rw is_monoid_hom.map_mul ⇑((s.ι).app r_j) },
id └───────────────────┘ ┴ └─┘ └─┘
src └─┘└───────────────────┘┴┴ └─┘└────┘ └┘
typ └─┘└───────────────────┘┴┴ └─┘└────┘└─┘└┘
doc └─┘└───────────────────┘┴ └────┘ └┘
txt └─┘ ┴ └────┘ └┘
par └─┘ ┴ └────┘ └┘
pid ┴ ┴ └────┘ ┴┴
st ─────┘└────────────────────────────────────────┘└┘└
178 -- one
st ───────────
179 { erw is_monoid_hom.map_one ⇑((s.ι).app r), refl },
id └───────────────────┘ └─┘ ┴
src └──┘└───────────────────┘┴ └─┘└────┘ ┴ └───┘
typ └──┘└───────────────────┘┴ └─┘└────┘┴┴ └───┘
doc └──┘ ┴ └────┘ ┴ └───┘
txt └──┘ ┴ └────┘ ┴ └───┘
par └──┘ ┴ └────┘ ┴ └───┘
pid ┴ ┴ └────┘ ┴ ┴
st ─────┘└──────────────────────────────────────┘└─────┘└┘└
180 -- mul_1
st ─────────────
181 { rw r_ih, },
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└─────┘└──┘└
182 -- mul_2
st ─────────────
183 { rw r_ih, },
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└─────┘└──┘└
184 -- mul_assoc
st ─────────────────
185 { rw mul_assoc, },
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└──────────┘└──┘└
186 -- one_mul
st ───────────────
187 { rw one_mul, },
id └─────┘
src └─┘└─────┘
typ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└────────┘└──┘└
188 -- mul_one
st ───────────────
189 { rw mul_one, } }
id └─────┘
src └─┘└─────┘
typ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─────
190 end
st ──┘
191
192 @[simp] def desc_morphism (s : cocone F) : colimit F ⟶ s.X :=
id └────┘ ┴ └─────┘ ┴ ┴ ┴└┘
src └────┘ └─────┘ ┴ └┘
typ └────┘ ┴ └─────┘ ┴ ┴ ┴└┘
doc └──┘ └────┘
193 { to_fun := desc_fun F s,
id └──────┘ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴
194 map_one' := rfl,
id └─┘
src └─┘
typ └─┘
195 map_mul' := λ x y, by { induction x; induction y; refl }, }
id ┴ ┴ ┴ ┴
src └────────┘ └────────┘ └───┘
typ ┴ ┴ └────────┘┴ └────────┘┴ └───┘
doc └────────┘ └────────┘ └───┘
txt └────────┘ └────────┘ └───┘
par └────────┘ └────────┘ └───┘
pid ┴ ┴ ┴
st └────────────────────────────────┘└┘
196
197 def colimit_is_colimit : is_colimit (colimit_cocone F) :=
id └────────┘ └────────────┘ ┴
src └────────┘ └────────────┘
typ └────────┘ └────────────┘ ┴
doc └────────┘
198 { desc := λ s, desc_morphism F s,
id ┴ ┴ └───────────┘ ┴ ┴
src ┴ └───────────┘
typ ┴ ┴ └───────────┘ ┴ ┴
doc ┴
199 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
200 begin
st └─────
201 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ──────┘└─
202 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
203 induction x,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
204 { have w' := congr_fun (congr_arg (λ f : F.obj x_j ⟶ s.X, (f : F.obj x_j → s.X)) (w x_j)) x_x,
id └───────┘ └───────┘ └───┘ ┴ └───┘ └─┘ ┴ └─┘ └─┘
src └─────────┘└───────┘┴ └───────┘┴ └───┘ ┴ ┴┴┴ └┘ └─┘└───┘┴ ┴ ┴└─┘└─┘ ┴ └─┘
typ └─────────┘└───────┘┴ └───────┘┴ └───┘└───┘┴ ┴┴┴ └┘ └─┘└───┘┴ ┴ ┴└─┘└─┘ ┴┴└─┘└─┘└─┘
doc └─────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘
txt └─────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘
par └─────────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘
pid └─────┘┴└─┘ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘
st ─────┘└─────────────────────────────────────────────────────────────────────────────────────────┘└─
205 erw w',
id └┘
src └──┘
typ └──┘└┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st ───────────┘└─
206 refl, },
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────────┘└──┘└
207 { simp only [desc_morphism, quot_one],
id └───────────┘ └──────┘
src └─────────┘└───────────┘└┘└──────┘┴
typ └─────────┘└───────────┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────┘└─────────────────────────────────┘└─
208 erw is_monoid_hom.map_one ⇑m,
id └───────────────────┘ ┴┴
src └──┘└───────────────────┘┴┴
typ └──┘└───────────────────┘┴┴┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ─────────────────────────────────┘└─
209 refl, },
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────────┘└──┘└
210 { simp only [desc_morphism, quot_mul],
id └───────────┘ └──────┘
src └─────────┘└───────────┘└┘└──────┘┴
typ └─────────┘└───────────┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────┘└─────────────────────────────────┘└─
211 erw is_monoid_hom.map_mul ⇑m,
id └───────────────────┘ ┴
src └──┘└───────────────────┘┴
typ └──┘└───────────────────┘┴ ┴
doc └──┘└───────────────────┘┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ─────────────────────────────────┘└─
212 rw [x_ih_a, x_ih_a_1],
id └────┘ └──────┘
src └──┘ └┘ ┴
typ └──┘└────┘└┘└──────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────┘└────────┘┴└─
213 refl, },
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────────┘└──┘└
214 refl
src └────
typ └────
doc └────
txt └────
par └────
pid └
st ─────────
215 end }.
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
216
217 instance has_colimits_Mon : has_colimits.{v} Mon.{v} :=
id └──────────┘ └─┘
src └──────────┘ └─┘
typ └──────────┘ └─┘
doc └──────────┘ └─┘
218 { has_colimits_of_shape := λ J 𝒥,
id ┴ ┴
typ ┴ ┴
219 { has_colimit := λ F, by exactI
id ┴
src └──────
typ ┴ └──────
doc └──────
txt └──────
par └──────
pid └
st └───────
220 { cocone := colimit_cocone F,
id └────────────┘
src ───┘ └─────────┘└────────────┘┴ └─
typ ───┘ └─────────┘└────────────┘┴ └─
doc ───┘ └─────────┘ ┴ └─
txt ───┘ └─────────┘ ┴ └─
par ───┘ └─────────┘ ┴ └─
pid ───┘ └─────────┘ ┴ └─
st ──────────────────────────────────
221 is_colimit := colimit_is_colimit F } } }
id └────────────────┘ ┴
src ───────────────────┘└────────────────┘┴ └─┘
typ ───────────────────┘└────────────────┘┴┴└─┘
doc ───────────────────┘ ┴ └─┘
txt ───────────────────┘ ┴ └─┘
par ───────────────────┘ ┴ └─┘
pid ───────────────────┘ ┴ └┘┴
st ──────────────────────────────────────────┘
222
223 end Mon.colimits